//
//  bmc.h
//  ltlbmc
//
//
//

#ifndef ltlbmc_bmc_h
#define ltlbmc_bmc_h

#include <vector>
#include "tree.h"
#include "ast.h"


using namespace cilast;

class bmc {
private:
    file* cfile;
    std::vector<treeNode*>* currlist;
    std::vector<treeNode*>* todolist;
    std::vector<treeNode*>* leaflist;

    int maxUnroll;
    int maxRec;
    
    void push(treeNode*);
    treeNode* pop();
    void swap();
    
    void explore();
    
    bool isWitness();
    bool isStop();

    
public:
    
    bmc(file* file);
    void run(int maxUnroll, int maxRec);
    
};

#endif
